T:Type, f:(TT), x, y:T, L:(T List). x=f*(y) via L  {(x  L) & (y  L)} 

latex

Definitions	b, hd(l), type List, s = t, t  T, Type, x:AB(x), a < b, (x  l), <a, b>, , A, x:A  B(x), P & Q, x:A. B(x), Void, P  Q, False, x:A. B(x), ||as||, #$n, , last(L), n+m, l[i], f(a), n - m, {i..j}, {x:A| B(x)} , [car / cdr], left + right, P  Q, P  Q, P  Q, A c B, y=f*(x) via L, {T}
Lemmas	fun-path wf, l member subtype, hd member, l member wf, last member, not wf, false wf, assert wf